$\forall$$R$:Realizer, $i$:Id. R{-}Feasible($R$) $\Rightarrow$ R{-}ds($R$;$i$) $=$ 1of([[$R$]]($i$)) $\in$ $x$:Id fp$\rightarrow$ Type